To cope with the high complexity of modern hardware design, designers can adopt a methodology that starts with a very high-level design specification. Such high-level specification can also be referred to as a high-level model (HLM). An HLM captures basic functionality of the design, but can leave out implementation details. The focus can therefore be on algorithm design and design exploration, since even extensive changes in the HLM's architecture can be easily made. Furthermore, a methodology using HLMs enables validation of the architecture during the early stages of design. HLMs can be written in a high-level programming language, such as C or C++.
Once the HLM has been validated, and sufficient decisions have been made regarding implementation of the design, the HLM can be refined to an RTL model (RTLM), that can then be processed by more “back-end” tools that perform synthesis and placement. The process of producing the RTLM from the HLM, however, is often performed in a mainly manual fashion that is error prone. A need therefore exists for EDA tools to assist the designer in verifying that the RTLM adheres to (or is equivalent to) the HLM.
A known approach for determining equivalence between an RTLM and HLM is the running of extensive simulations on both models. The results of such simulations are compared. Such simulations can be very time consuming and can miss subtle discrepancies between the two models.
Therefore, there exists a need for better methods of determining equivalence between RTLMs and HLMs. A formal approach to determining such equivalency is desirable since such approaches have the possibility of actually proving that, according to some standard of equivalency, the two models are equivalent.
However, conventional approaches to formal analysis are often too inefficient when applied to anything but small scale designs. What is needed, therefore, are more efficient approaches to formal analysis that have a good expectation of proving equivalency between large-scale designs.
In addition to the formal analysis itself, issues that can also be addressed, for improving the efficiency of formal approaches to equivalence determination, include the following: producing an appropriate common representation of the RTLM and HLM; producing an appropriate test bench for combining the RTLM and HLM; and determining appropriate initial conditions from which to start a formal analysis.